Termination w.r.t. Q of the given QTRS could be disproven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(b(c(x1))) → c(b(a(x1)))
a(c(x1)) → a(a(d(a(x1))))
d(a(b(x1))) → b(a(d(x1)))
d(a(c(x1))) → b(c(c(x1)))

Q is empty.

(1) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.

Found the self-embedding DerivationStructure:

a (a b)^k+1 c c → a (a b)^k+2 c c

a (a b)^k+1 c c → a (a b)^k+2 c c
by Overlap u with r (ol3)

a (a b)^k+1 c → a a (b a)^k+1 d a
by Overlapping Derivationstructures

a (a b)^k+1 c → a a d (a b)^k+1 a
by Overlap u with l (ol4)

(a b)^k+1 c → c b (a b)^k a
by Operation rotate

(a b)^k+1 c → c (b a)^k+1
by Operation lift

(a b)^k c → c (b a)^k
by Selfoverlapping OC am1

a b c → c b a
by original rule (OC 1)

a c → a a d a
by original rule (OC 1)

d (a b)^k+1 → (b a)^k+1 d
by Operation lift

d (a b)^k → (b a)^k d
by Selfoverlapping OC am2

d a b → b a d
by original rule (OC 1)

d a c → b c c
by original rule (OC 1)

(2) NO